#ifndef _ANNODEFS_H_
#define _ANNODEFS_H_

#define SPECSTRINGIZE( x ) #x

#ifdef _PREFAST_

#define __requires(expr)                __declspec("HAVOC_pre")   __declspec("HAVOC_assert("SPECSTRINGIZE(expr)")")
#define __ensures(expr)                 __declspec("HAVOC_post")  __declspec("HAVOC_assert("SPECSTRINGIZE(expr)")")
#define __free_requires(expr)           __declspec("HAVOC_pre")   __declspec("HAVOC_assume("SPECSTRINGIZE(expr)")")
#define __free_ensures(expr)            __declspec("HAVOC_post")  __declspec("HAVOC_assume("SPECSTRINGIZE(expr)")")
#define __cand_requires(expr)           __declspec("HAVOC_pre")   __declspec("HAVOC_cand_assert("SPECSTRINGIZE(expr)")")
#define __cand_ensures(expr)            __declspec("HAVOC_post")  __declspec("HAVOC_cand_assert("SPECSTRINGIZE(expr)")")
#define __modifies(expr)                __declspec("HAVOC_modifies("SPECSTRINGIZE(expr)")")
#define __frees(expr)                   __declspec("HAVOC_frees("SPECSTRINGIZE(expr)")")
#define __modifies_resource(res,expr)   __declspec("HAVOC_modifies_resource(" # res ","SPECSTRINGIZE(expr)")")
#define __modifies_global_resource(res) __declspec("HAVOC_modifies_global_resource(" # res ")")
#define __modifies_field(field,expr)   __declspec("HAVOC_modifies_field("SPECSTRINGIZE(field)","SPECSTRINGIZE(expr)")")
#define __modifies_type(type,expr)   __declspec("HAVOC_modifies_type("SPECSTRINGIZE(type)","SPECSTRINGIZE(expr)")")
#define __may_throw(expr)               __declspec("HAVOC_may_throw("SPECSTRINGIZE(expr)")")

#define __instrument_read(field,when)       __declspec("HAVOC_instrument_read(" # field "," # when ")")
#define __instrument_write(field,when)      __declspec("HAVOC_instrument_write(" # field "," # when ")")
#define __instrument_address(field,when)    __declspec("HAVOC_instrument_address(" # field "," # when ")")
#define __instrument_increment(field,when)  __declspec("HAVOC_instrument_increment(" # field "," # when ")")
#define __instrument_decrement(field,when)  __declspec("HAVOC_instrument_decrement(" # field "," # when ")")

#define __instrument_call(field,when,func)          __declspec("HAVOC_instrument_call(" # field "," # when "," # func ")")
#define __instrument_call_bind_return(ret)          __declspec("HAVOC_instrument_call_bind_return(" # ret ")")
#define __instrument_call_bind_argument(num,arg)    __declspec("HAVOC_instrument_call_bind_argument(" # num "," #arg ")")

#define __instrument_all_template                   __declspec("HAVOC_instrument_all_template")
#define __instrument_types_template(arg)            __declspec("HAVOC_instrument_types_template(" # arg ")")

#define __instrument_universal_all                  __declspec("HAVOC_instrument_universal_all")
#define __instrument_universal_type(arg)            __declspec("HAVOC_instrument_universal_type(" # arg ")")
#define __instrument_universal_include(X)           __declspec("HAVOC_instrument_universal_include(" # X ")")
#define __instrument_universal_exclude(X)           __declspec("HAVOC_instrument_universal_exclude(" # X ")")

#define __instrument_loop_all                       __declspec("HAVOC_instrument_loop_all")
#define __instrument_loop_template                  __declspec("HAVOC_instrument_loop_template")	


#define __field_equiv(field1,field2)    __declspec("HAVOC_field_equiv("SPECSTRINGIZE(field1)","SPECSTRINGIZE(field2)")")
#define __type_equiv(field)             __declspec("HAVOC_type_equiv("SPECSTRINGIZE(field)")")
#define __instrument_field_equiv(ANNOT)     ANNOT void __instrument_internal_field_equiv(){}

#define __type_extend(annot)            __declspec("HAVOC_type_extend("SPECSTRINGIZE(annot)")")

#define __override_type(expr)           __declspec("HAVOC_override_type(" # expr ")")
#define __function_type(name)                   __declspec("HAVOC_function_type(\"" # name "\")")

#define __type_var(v)		        __declspec("HAVOC_type_var(" #v ")")
#define __instrument_type_var(t)	__type_var(x) void __instrument_type_var_##t (t x) { }

#define __async_call                        do { __requires(1) void __havoc_async_call(); } while (0);
#define __loop_invariant(ANNOT)             do { ANNOT void __havoc_loop_invariant(); } while (0);
#define __call_invariant(ANNOT)             do { ANNOT void __havoc_call_invariant(); } while (0);
#define __analysis_hv_assert(expr)          do { __requires(expr) void __havoc_assert(); } while (0);
#define __analysis_hv_assume(expr)          do { __ensures(expr)  void __havoc_assume(); } while (0);
#define __hv_updates_resource(res, addr, val)          do { __requires(__imperative_updates_resource(res, addr, val)) void __havoc_imperative_updates_resource(); } while (0);

#define __bpl_attribute(k,v)		__declspec("HAVOC_bpl_attribute(" #k "," #v ")")

#define __declare_havoc_bvar_type(x,t)  t x

#else // _PREFAST_

#define __requires(e)
#define __ensures(e)
#define __free_requires(e)
#define __free_ensures(e)
#define __cand_requires(e)
#define __cand_ensures(e)
#define __modifies(expr)
#define __frees(expr)
#define __modifies_resource(res,expr)
#define __modifies_global_resource(res)
#define __modifies_field(field,expr)
#define __modifies_type(type,expr)
#define __may_throw(expr)

#define __instrument_read(field,when)
#define __instrument_write(field,when)
#define __instrument_address(field,when)
#define __instrument_increment(field,when)
#define __instrument_decrement(field,when)

#define __instrument_call(field,when,func)
#define __instrument_call_bind_return(ret)
#define __instrument_call_bind_argument(num,arg)

#define __instrument_all_template 
#define __instrument_types_template(arg)

#define __instrument_universal_all
#define __instrument_universal_type(arg)
#define __instrument_universal_include(X)
#define __instrument_universal_exclude(X)

#define __instrument_loop_all
#define __instrument_loop_template

#define __field_equiv(field1,field2)
#define __type_equiv(field)
#define __instrument_field_equiv(ANNOT)     

#define __type_extend(annot)

#define __override_type(expr)
#define __function_type(name)

#define __type_var(v)
#define __instrument_type_var(t)


#define __async_call
#define __loop_invariant(ANNOT)
#define __call_invariant(ANNOT)
#define __analysis_hv_assert(expr)
#define __analysis_hv_assume(expr)
#define __hv_updates_resource(res, addr, val)

#define __analysis_hv_nothrow
#define __analysis_hv_noinstrument(func)

#define __bpl_attribute(k,v)

#define __declare_havoc_bvar_type(x,t) 
#endif

#define __instrument_read_pre(field)        __instrument_read(field,1)
#define __instrument_read_post(field)       __instrument_read(field,0)
#define __instrument_write_pre(field)       __instrument_write(field,1)
#define __instrument_write_post(field)      __instrument_write(field,0)
#define __instrument_address_pre(field)     __instrument_address(field,1)
#define __instrument_address_post(field)    __instrument_address(field,0)
#define __instrument_increment_pre(field)   __instrument_increment(field,1)
#define __instrument_increment_post(field)  __instrument_increment(field,0)
#define __instrument_decrement_pre(field)   __instrument_decrement(field,1)
#define __instrument_decrement_post(field)  __instrument_decrement(field,0)
#define __instrument_call_pre(field,func)   __instrument_call(field,1,func)
#define __instrument_call_post(field,func)  __instrument_call(field,0,func)


#define SET_CONTAINING_RECORD(set, decr_off, incr_off) __set_incr(__set_decr(set, decr_off), incr_off)
#define HNULL 0

#define disjoint(a, b) __disjoint(a,b)
#define disjoint3(a, b, c) __and(disjoint(a,b), __and(disjoint(b,c), disjoint(a,c)))
#define disjoint4(a, b, c, d) __and(disjoint3(a,b,c), __and(disjoint(a,d), __and(disjoint(b,d), disjoint(c,d))))
#define disjoint5(a, b, c, d, e) __and(disjoint4(a,b,c,d), __and(disjoint(a,e), __and(disjoint(b,e), __and(disjoint(c,e), disjoint(d,e)))))

#define distinct(a, b) __disjoint(__set(a), __set(b))
#define distinct3(a, b, c) __and(distinct(a,b), __and(distinct(b,c), distinct(a,c)))
#define distinct4(a, b, c, d) __and(distinct3(a,b,c), __and(distinct(a,d), __and(distinct(b,d), distinct(c,d))))
#define distinct5(a, b, c, d, e) __and(distinct4(a,b,c,d), __and(distinct(a,e), __and(distinct(b,e), __and(distinct(c,e), distinct(d,e)))))

// can write a function __annotations VOID __prototype(X, Function) (...); and have the __annotations
// be added to the actual function during analysis. useful for inferred or other auto-generated annotations
#define __prototype(WHERE, FUNC)    __prototype##WHERE##_##FUNC


#define __attribute(k,v)				        __bpl_attribute( #k , #v )
#define __concurrent					        __attribute( concurrent , 1 )
#define __syncopr						__attribute( syncopr , 1 )
#define __async							__attribute( async , 1 )
#define __yield							__attribute( yield , 1 )
#define __inlined						__attribute( inline , 1 )
#define __usespec						__attribute( usespec , 1 )
#define __repeat						__attribute( repeat , 1 )

//extracting the field for use in __btwn, __set_incr, __set_decr.
#define __field(PType, field) 					__offset((*((PType)0)).##field##)

#define __base(e)						__objectOf(e)


//short hands
#define __hv_assert(e)                                         __analysis_hv_assert(e)
#define __hv_assume(e)                                         __analysis_hv_assume(e)
//loop assertions
#define __loop_assert(e)					__requires(e)
#define __loop_free_assert(e)					__free_requires(e)
#define __loop_modifies(e)					__modifies(e)
#define __loop_modifies_resource(r,e)				__modifies_resource(r, e)
#define __loop_modifies_global_resource(r,e)			__modifies_global_resource(r, e)

#define __declare_havoc_bvar(x)                                 __declare_havoc_bvar_type(x, int*)

#endif // _ANNODEFS_H_
